header {
/*******************************************************************************
 * Copyright (c) 2009 Kevin Bierhoff and others.
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *     Kevin Bierhoff - initial API and implementation
 *******************************************************************************/
package com.googlecode.twelfdevtools.twelfparser;

import java.util.List;
import java.util.LinkedList;

import com.googlecode.twelfdevtools.twelfast.*;
}
class TwelfParser extends Parser;
options { k = 3; }

startRule returns [List<ITwelfDeclaration> decls]
{ decls = new LinkedList<ITwelfDeclaration>(); ITwelfDeclaration d; }
	: 	(d=decl { decls.add(d); })*
	;

decl returns [ITwelfDeclaration decl]
{ decl = null; }
	:	decl=constant
	;
	
constant returns [ConstantDeclaration decl]
{ ITwelfTerm t = null, v = null; decl = null; }
	: 	c:ID 
		(	":" t=term ("=" v=term)? 
		| 	"=" v=term
		) e1:"."
		{ Identifier w = new Identifier(c.getText(), c.getLine(), c.getColumn()); decl = ConstantDeclaration.namedConst(w, t, v, c.getLine(), c.getColumn(), e1.getLine(), e1.getColumn() + 1); }
	| 	b:"_" (":" t=term)? "=" v=term e2:"."
		{ decl = ConstantDeclaration.anonConst(t, v, b.getLine(), b.getColumn(), e2.getLine(), e2.getColumn() + 1); }
	;
	
term returns [ITwelfTerm t]
{ t = null; }
	:	t=pi_term
	;
	
pi_term returns [ITwelfTerm result]
{ ITwelfTerm vt = null, t; result = null; }
	: 	"{" x:ID (":" vt=term)? "}" t=pi_term
		{ Identifier v = new Identifier(x.getText(), x.getLine(), x.getColumn()); result = Pi.pi(v, vt, t); }
	| 	"[" c:ID (":" vt=term)? "]" t=pi_term
		{ Identifier w = new Identifier(c.getText(), c.getLine(), c.getColumn()); result = Lambda.lambda(w, vt, t); }
	| 	result=ascr_term
	;
	
ascr_term returns [ITwelfTerm result]
{ ITwelfTerm t, a; result = null; }
	: 	t=arr_term 
		(	":" a=term 
			{ result = Ascription.ascr(t, a); }
		| 	{ result = t; } 
		)
	;
	
arr_term returns [ITwelfTerm result]
{ ITwelfTerm t1, t2; result = null; LinkedList<ITwelfTerm> stack = new LinkedList<ITwelfTerm>(); }
	: 	t1=app_term 
		(	"->" t2=app_term
			{ stack.add(t1); t1 = t2; } 
		|	"<-" t2=app_term 
			{ t1 = Arrow.backArr(t1, t2); } 
		)*
		{ stack.add(t1); result = Arrow.forwArr(stack); }
	;
	
app_term returns [ITwelfTerm result]
{ ITwelfTerm t2; result = null; }
	:	result=atom_term 
		(	t2=atom_term
			{ result = Application.app(result, t2); } 
		)*
	;
	
atom_term returns [ITwelfTerm result]
{ result = null; }
	: "type"	{ result = Type.type(); }
	| w:"_"		{ result = new Wildcard(w.getLine(), w.getColumn()); }
	| x:ID		{ result = new Identifier(x.getText(), x.getLine(), x.getColumn()); }
	| "(" result=term ")"
	;
	

class TwelfLexer extends Lexer;
options { k = 3; }
{
public void tab() {
	// count tab as regular column, like eclipse does
	setColumn( getColumn() + 1 );
}
}

ID 
	: ('A'..'Z' | 'a'..'z' | '0'..'9' | '-' | '/' | '>' | '<' | '_' | '\'')+
	;
	
CONTROL
	: ':' | '.' | '(' | ')' | '[' | ']' | '{' | '}' 
	;
	
COMMENT
	: '%' 
	(	'\n' { newline(); }
	|	('%'|' ') (~'\n')* '\n' { newline(); }
	|	'{' 
		(	{ LA(2) != '%' }? '}'
		|	'\n' { newline(); }
		|	~('}'|'\n')
		)* 
		"}%"
	) 
	{ $setType(Token.SKIP); }
	;

PRAGMA
	: '%' ('a'..'z') (~'\n')* '\n' { newline(); $setType(Token.SKIP); }
	;

WS  :   (' '
    |   '\t'
    |   '\n' { newline(); }
    |   '\r')+
        { $setType(Token.SKIP); }
    ;
